00050	VAR: X1,X2,X3,X4,x,y,z,u,v; PRE_PRED:M,D,P;PRE_OP:C,B,A,F,S;
00100	¬D(X1,C) ∨ ¬D(X1,B);
00200	M(X1,S(F(X1,X2)),S(X3)) ∨ ¬M(X1,S(X3),S(X2))∨  ¬D(X1,X2);
00300	D(X1,X3) ∨ D(X1,X2) ∨ ¬P(X1) ∨ ¬M(X2,X3,X4) ∨ ¬D(X1,X4);
00400	D(X1,X3) ∨ ¬M(X1,X2,X3);
00500	M(X2,X1,X3) ∨ ¬M(X1,X2,X3);
00600	M(X1,X1,S(X1));
00800	M(A,S(C),S(B));
01000	THEOREM:¬P(A);
01100	;